#include "check.h"
#include <assert.h>
#include <iostream>
#include <string>
#include <cstdio>
#include <cmath>
#include <statesFileLexer.h>
#include <statesFileParser.h>

#define toBOOL(a) (a?TRUE:FALSE)

using namespace std;

const int TRUE=1, FALSE=0;

void getStates(const string & assignmentFile, State & init, State & final)
{
	// Example of a grammar for parsing C sources,
	// Adapted from Jim Idle (jimi cut-this at idle ws) excluding the lengthy comments which were removed for convenience

	pANTLR3_UINT8	fName;
	pANTLR3_INPUT_STREAM    input;
	pstatesFileLexer		lxr;
	pANTLR3_COMMON_TOKEN_STREAM	    tstream;
	pstatesFileParser	psr;
	fName	= (pANTLR3_UINT8)assignmentFile.c_str();

	input	= antlr3AsciiFileStreamNew(fName);
	if ( input == NULL)
	{
		fprintf(stderr, "Failed to open file %s\n", (char *)fName);
		exit(1);
	}

	lxr	    = statesFileLexerNew(input);

	if ( lxr == NULL )
	{
		fprintf(stderr, "Unable to create the lexer due to malloc() failure1\n");
		exit(1);
	}
	tstream = antlr3CommonTokenStreamSourceNew(ANTLR3_SIZE_HINT, TOKENSOURCE(lxr));

	if (tstream == NULL)
	{
	fprintf(stderr, "Out of memory trying to allocate token stream\n");
	exit(1);
	}
	psr	    = statesFileParserNew(tstream);

	if (psr == NULL)
	{
		fprintf(stderr, "Out of memory trying to allocate parser\n");
		exit(ANTLR3_ERR_NOMEM);
	}

	//Here are our main code changes to that of Jim Idle
	psr->getInitialState(psr,init.variables);
	psr->getFinalState(psr,final.variables);
	 //Here is all what we added


	psr	    ->free  (psr);	    psr = NULL;
	tstream ->free  (tstream);	    tstream = NULL;
	lxr	    ->free  (lxr);	    lxr = NULL;
	input   ->close (input);	    input = NULL;

}

class TraversalCheck
{
private:
	NewGraph * graph;

	int evaluateExp(NewGraph::ProgNode * exp,const State & actualFinal, bool &unsupported)
	{
		unsupported=false;
		assert(exp!=NULL);
		NewGraph::NodeType node_type=exp->type();
		NodeType t=exp->data->type;
		if (t==ERROR_NODE)
		{
			cout<< "Reached a compilor error, unable to check model.\n";
			unsupported=true;
			return -1;
		}
		switch(node_type)
		{
		case NewGraph::Literal:
			{
				int val;
				NewGraph::ProgLit * lit=(NewGraph::ProgLit *)exp;
				sscanf(lit->value.c_str(),"%d",&val);
				return val;
			}
		case NewGraph::Variable:
			{
				NewGraph::ProgVar * var=(NewGraph::ProgVar *)exp;
				string & name= var->name;
				VariablesMap::const_iterator it=actualFinal.variables.find(name);
				if (it==actualFinal.variables.end())
				{
					cout<<"Variable "<<name<<" used but not declared.\n";
					unsupported=true;
					return -1;
				}
				else
				{
					NodeType type=it->second.type->type;
					if (type!=INT_TYPE && type!=BOOL_TYPE)
					{
						cout<<"No support for the use of variables of type different from 'int' or 'bool'.\n";
						unsupported=true;
						return -1;
					}
					else
					{
						if (!it->second.set)
						{
							cout<<"Variable "<<name<<" un-initialized before use.\n";
							unsupported=true;
							return -1;
						}
						if (it->second.unsupported_value)
						{
							unsupported=true;
							return -1;
						}
						else
							return it->second.value;
					}
				}
			}
		case NewGraph::Expression:
			{
				if (t==ARRAY_OP || t==PAIR_OP)
				{
					unsupported=true;
					return -1;
				}
				const string & op=exp->data->getAdditionalTag();
				int val1,val2;
				//cout<<op<<"\n";
				if (op!="!")
				{
					NewGraph::ProgNode * left=graph->getChild(exp,LEFT),
									   * right=graph->getChild(exp,RIGHT);
					assert (left!=NULL && right!=NULL);
					val1=evaluateExp(left,actualFinal,unsupported);
					if (unsupported)
						return -1;
					val2=evaluateExp(right,actualFinal,unsupported);
					if (unsupported)
						return -1;
				}
				else
				{
					NewGraph::ProgNode * of=graph->getChild(exp,OF_EDGE);
					assert (of!=NULL);
					val1=evaluateExp(of,actualFinal,unsupported);
					if (unsupported)
						return -1;
					val2=-1; //not used anyways...
				}
				if (op=="+") //arithmetic ops
					return (val1+val2);
				else if (op=="-")
					return (val1-val2);
				else if (op=="*")
					return (val1*val2);
				else if (op=="/")
					return (val1/val2);
				else if (op=="^")
					return (int)pow((double)val1,(double)val2);
				else if (op=="%")
					return (val1%val2);

				else if (op=="<") //comparisons
					return toBOOL(val1<val2);
				else if (op==">")
					return toBOOL(val1>val2);
				else if (op=="<=")
					return toBOOL(val1<=val2);
				else if (op==">=")
					return toBOOL(val1>=val2);
				else if (op=="==")
					return toBOOL(val1==val2);
				else if (op=="!=")
					return toBOOL(val1!=val2);

				else if (op=="&&") //boolean ops
					return toBOOL((bool)val1 && (bool)val2);
				else if (op=="||")
					return toBOOL((bool)val1 || (bool)val2);
				else if (op=="=>")
					return toBOOL(!(bool)val1 ||(bool)val2);
				else if (op=="<=>")
					return toBOOL(val1==val2 && (val2==TRUE || val2==FALSE));
				else if (op=="<>")
					return toBOOL((!(bool)val1 && (bool)val2) || ((bool)val1 && !(bool)val2));
				else if (op=="!")
					return toBOOL(!(bool)val1);
				else
					throw -1;
			}
		default:
			throw -1;
		}
	}

public:
	TraversalCheck(NewGraph * graph)
	{
		this->graph=graph;
		/*stringstream ss (stringstream::in | stringstream::out);
		ss<<"[ ";
		for (int i=0;i<v.size();i++)
		{
			ss<<v[i].toString();
			if (i<v.size()-1)
				ss<<"\n";
		}
		ss<<" ]";
		return ss.str();*/
	}
	bool traverseCode(NewGraph::ProgNode * node, State & actualFinal)
	{
		NewGraph::NodeType type=node->type();
		assert(type==NewGraph::Statement);
		NodeType t=node->data->type;
		switch(t)
		{
		case DECL://add variable to actualFinal state if not there, otherwise (check for consistency of the types, or just ignore)
			{
				NewGraph::ProgVar * var=(NewGraph::ProgVar *)graph->getChild(node,VARNAME);
				assert (var!=NULL);
				string & name= var->name;
				VariablesMap::iterator it=actualFinal.variables.find(name);
				if (it!=actualFinal.variables.end())
				{
					if (!var->data->equals(it->second.type))
					{
						cout<<"Inconsistent Types between code and that of check model.\n";
						return false;
					}
				}
				else
				{
					actualFinal.variables.insert(VariablesPair(name,VariableInfo(var->data)));
					//we will not check here if array or not, since it may be declared but not used
				}
				break;
			}
		case ASSIGN_ST: //change value of variable in actual final, use some helper functions to evaluate the expressions
			{
				NewGraph::ProgVar * var=(NewGraph::ProgVar *)graph->getChild(node,LEFT);
				assert (var!=NULL);
				NodeType t=var->data->type;
				if (t!=INT_TYPE && t!=BOOL_TYPE)
				{
					//cout<<"No support for Array operators or pair operators.\n";
					//return false;
					break; //no need to return false, we can ignore array or pair statements that dont affect our variables
				}
				string & name= var->name;
				VariablesMap::iterator it=actualFinal.variables.find(name);
				if (it==actualFinal.variables.end())
				{
					cout<<"Variable "<<name<<" un-initialized before use.\n";
					return false;
				}
				else
				{
					bool unsupported;
					NewGraph::ProgNode * exp=graph->getChild(node,RIGHT);
					assert (exp!=NULL);
					int val=evaluateExp(exp,actualFinal,unsupported);
					if (unsupported)
						it->second.unsupported_value=true;
					else
						it->second.setValue(val);
				}
				break;
			}
		case IF_ST: //depending on the value of the condition, call traverseCode to the body of if or else
			{
				bool unsupported;
				NewGraph::ProgNode * exp=graph->getChild(node,CONDITION);
				assert (exp!=NULL);
				int value=evaluateExp(exp,actualFinal,unsupported);
				if (unsupported)
					return false;

				NewGraph::ProgNode * if_st=graph->getChild(node, IF_STATEMENTS);
				NewGraph::ProgNode * else_st=graph->getChild(node, ELSE_STATEMENTS);
				assert (if_st!=NULL);
				if (value==TRUE)
				{
					if (!traverseCode(if_st,actualFinal))
						return false;
				}
				else
				{
					if (else_st!=NULL)
						if (!traverseCode(else_st,actualFinal))
							return false;
				}
				break;
			}
		case WHILE_ST: //depending on the value of the condition, call multiple of times the traverseCode on the boby of the while statements
			{
				bool unsupported;
				NewGraph::ProgNode * exp=graph->getChild(node,CONDITION);
				assert (exp!=NULL);
				int value=evaluateExp(exp,actualFinal,unsupported);
				if (unsupported)
					return false;

				NewGraph::ProgNode * while_st=graph->getChild(node, WHILE_STATEMENTS);
				assert (while_st!=NULL);
				while (value==TRUE)
				{
					if (!traverseCode(while_st,actualFinal))
						return false;
					value=evaluateExp(exp,actualFinal,unsupported); //no need to check for unsupported, since evaluated before than for sure, is supported or has left function prior to this statement
				}
				break;
			}
		case ERROR_NODE:
			cout<< "Reached a compilor error, unable to check model.\n";
			return false;
		default:
			;//ignore the rest of statements
		}
		//move to the next statement
		NewGraph::ProgNode * nextNode=graph->getChild(node, NEXT_STATEMENT);
		if (nextNode==NULL)
			return true;
		else
			return traverseCode(nextNode,actualFinal);
	}

};

CheckResult consistent(const State & s1, const State & s2)//we assume s1 is smaller State than s2
{
	CheckResult return_val=CONSISTENT;
	VariablesMap::const_iterator it1;
	for (it1=s1.variables.begin(); it1!=s1.variables.end();it1++)
	{
		string var=it1->first;
		VariablesMap::const_iterator it2=s2.variables.find(var);
		if (it2!=s2.variables.end())
		{
			NodeTypeInterface * dec= it1->second.type;
			bool isBasic=(dec->type==INT_TYPE || dec->type==BOOL_TYPE);
			int val1=it1->second.value, val2=it2->second.value;
			bool isConsistent=(val1==val2);
			bool unsupported=it2->second.unsupported_value;
			if (unsupported)
			{
				if (return_val!=CONFLICT)
					return_val=INCONCLUSIVE;
				if (it2->second.set)
					cout<<"Value of '"<<var<<"' had to be computed using unsupportted operations such as Array or Pair operations.\n";
			}
			else if (isBasic && !isConsistent)
			{
				return_val=CONFLICT;
				cout<<"Conflict at '"<<var<<"', expected '"<<val1<<"' while found '"<<val2<<"'\n";
			}
		}
	}
	return return_val;
}

CheckResult checkModel(NewGraph * graph, const string & assignmentFile)
{

	State init, assumedFinal,actualFinal;
	getStates(assignmentFile,init, assumedFinal);
	TraversalCheck check(graph);
	actualFinal=init;
	NewGraph::ProgNode * root=graph->vertices[0];
	bool completed=check.traverseCode(root,actualFinal);
	if (completed)
	{
		CheckResult comp=consistent(assumedFinal,actualFinal);
		cout<<CheckResult2string(comp)<<"!\n";
		return comp;
	}
	else
	{
		cout<<CheckResult2string(INCONCLUSIVE)<<"!\n";
		return INCONCLUSIVE;
	}
}
